Termination Proof Script

Consider the TRS R consisting of the rewrite rules

There are 8 dependency pairs:

The approximated dependency graph contains one SCC: {13,15,17}.

Consider the SCC {13,15,17}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(n__cons) = π(n__from) = 1 together with the lexicographic path order with empty precedence, the rules in {13,15} are weakly decreasing and rule 17 is strictly decreasing. There is one new SCC.
- Consider the SCC {13,15}. By taking the AF π with π(ACTIVATE) = π(n__cons) = 1 together with the lexicographic path order with empty precedence, rule 13 is weakly decreasing and rule 15 is strictly decreasing. There is one new SCC.
  - Consider the SCC {13}. By taking the AF π with π(ACTIVATE) = 1 and π(n__cons) = [1] together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.00 seconds) --- May 3, 2006